$\forall$${\it es}$:ES, ${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type). es{-}decl(${\it es}$;${\it ds}$;${\it da}$) $\in$ $\mathbb{P}$